COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Equations ({eq }), ({eq }) and ({eq }) can all be regarded as
C00005 ENDMK
C⊗;
Equations ({eq }), ({eq }) and ({eq }) can all be regarded as
axiom schemata in first order logic but containing a second
order functions %At%1.  Thus a sentence of first order logic
results from substituting a suitable functional for %At%1
and a suitable first order funtion for %Af%1 in ({eq }).
As long as we regard the schema as just a way of generating
a computable collection of first order formulas, there is
no reason to regard it as different in principle from a first
order schema.  However, we may conjecture that not every
collection of first order sentences that can be generated
by a second order schema can also be generated from a first
order schema.  There is a problem that not every second order
functional may be substituted for %At%1 in the schema; it has
to be continuous.  What this means in general is not clear.

Proving non-termination with finite approximation functions.

.bb "#. Going from the Functional qt to the Recursive Structure of the Program."

	Notice that the functional equation and the minimization
schema for a recursive definition are expressed directly in terms of
the functional %2qt[f](x)%1, while the schemata for inductive
assertions and subgoal induction involve the specific functions
that appear in the recursive definition.  We would like to express
these proof methods in terms of qt directly, but we have not succeeded
and the task seems difficult.

	This raises the question of whether we can retrieve the recursive
structure of the program from the functional and how to go about it.
For example, suppose we know that %2qt[f](x)%1 has the form

	%2qif p x qthen g x qelse f h x71.

Can we determine ⊗p, ⊗g and ⊗h from qt?